/*
 * PNCoverabilityTree.java
 *
 */

package edu.uj.petri.algorithms;

import edu.uj.petri.model.Marking;
import edu.uj.petri.model.Matrix;
import edu.uj.petri.model.Model;
import edu.uj.petri.model.Place;
import edu.uj.petri.model.Transition;
import java.util.Collection;
import java.util.HashSet;
import java.util.List;
import java.util.ResourceBundle;
import javax.swing.BoxLayout;
import javax.swing.JLabel;
import javax.swing.JPanel;
import javax.swing.JScrollPane;
import javax.swing.JTree;
import javax.swing.tree.DefaultMutableTreeNode;
import javax.swing.tree.DefaultTreeCellRenderer;

/**
 * Constructs coverability tree and graph. Also does analyses.
 * @author mkruk
 */
public class PNCoverabilityTree{
    
    private PNTreeNode rootNode = null;
    private Matrix incidenceMatrix = null;
    private Marking initialMarking = null;
    private Model model;
    boolean isBoundness = true;
    boolean isDead = false;
    String strHTML = "";
    
    /** Creates a new instance of PNCoverabilityTree */
    public PNCoverabilityTree(Model m) {
        this.model = m;
        this.incidenceMatrix = this.model.getIncidenceMatrix();
        this.initialMarking = this.model.getMarking();
        if(this.initialMarking.toArray().length != 0){
            this.rootNode = new PNTreeNode(this.initialMarking,"",PNTreeNode.Tag.NEW);
        }
        
    }
    
    
    /** Generates coverability tree
     * @param node starting node
     */
    public void Generate(PNTreeNode node){
        
        
        if(node.GetTag() == PNTreeNode.Tag.NEW){

            // tag as blank
            node.SetTag(PNTreeNode.Tag.BLANK);
            
            // get all active transition
            Collection<Transition> allTransitions = new HashSet<Transition>(model.getAllTransitions());         
          
            for(Transition t : allTransitions){
//System.out.println("To fire: " + t.getName());   
                // apply this node marking to net
                this.model.applyMarking(node.getMyMarking());
                if(t.canBeFired()){
                    
                    t.fire();
//System.out.println("Fired: " + t.getName());                
                    PNTreeNode newNode = new PNTreeNode(this.model.getMarking(),t.getName(),PNTreeNode.Tag.NEW);
                    
                    node.AddChildNode(newNode);
                    
                    if(newNode.CheckMarkingAndSetOmega()){
                        this.isBoundness = false;
                    }
                    
                    if(newNode.isOmegaMarking()){
                        newNode.SetTag(PNTreeNode.Tag.OLD);
                        //break;
                    }        
                    
                    if(newNode.HasEqualMarking()){
                       // tag as old and add
                        newNode.SetTag(PNTreeNode.Tag.OLD);
                    }else{
                        Generate(newNode);
                    }

                }
               
                
            }
            // if has no childnodes tag as deadend
            if(node.GetChildNodes().isEmpty()){
                node.SetTag(PNTreeNode.Tag.DEADEND);
                this.isDead = true;
            }
            
        }else{ // if blank, old, deadend - do not generate
            return;
        }
    }
    /** For internal use. Adds JTree TreeNode to treeview */
    private void AddNodesToTreeView(DefaultMutableTreeNode treeViewNode,PNTreeNode node){
        if(node.GetChildNodes().isEmpty()){
            return;
        }
        
        // for each child of node
        List tmp = node.GetChildNodes();
        for(int ii = 0;ii < tmp.size();++ii){
            // create new treeviewnode n
            DefaultMutableTreeNode next = new DefaultMutableTreeNode(((PNTreeNode) tmp.get(ii)).toString());
            treeViewNode.add(next);
            AddNodesToTreeView(next, (PNTreeNode) tmp.get(ii));
            
        }
        
    }
    
    /** For internal use. Adds JTree TreeNode to graph */
    private void AddNodesToGraph(DefaultMutableTreeNode treeViewNode,PNTreeNode node){
        // if meets leaf node with old tag prints only its transiton label
        if(node.GetChildNodes().isEmpty()){
            if(node.GetTag() == PNTreeNode.Tag.OLD){
                DefaultMutableTreeNode old = new DefaultMutableTreeNode(node.GetLabel());
                treeViewNode.add(old);
            }
            return;
        }
        
        // for each child of node
        List tmp = node.GetChildNodes();
        for(int ii = 0;ii < tmp.size();++ii){
            // create new treeviewnode n
            DefaultMutableTreeNode next = new DefaultMutableTreeNode(((PNTreeNode) tmp.get(ii)).toString());
            treeViewNode.add(next);
            AddNodesToGraph(next, (PNTreeNode) tmp.get(ii));
            
        }
        
        
    }
    /** Generates coverability graph. */
    public JTree BuildCoverabilityGraph(){
        
        DefaultMutableTreeNode root = new DefaultMutableTreeNode(this.rootNode.toString());
        AddNodesToGraph(root,this.rootNode);
        JTree tree = new JTree(root);
        DefaultTreeCellRenderer renderer = new DefaultTreeCellRenderer();
        renderer.setLeafIcon(null);
        renderer.setClosedIcon(null);
        renderer.setOpenIcon(null);
        tree.setCellRenderer(renderer);
        expandAllNodesInJTree(tree);
        
        return (tree);
    }
    
    /** Generates coverability tree, does analyse and generate JPanel with all needed components

     */
    public JPanel GetTree(){
        
        // TODO jesli inhibitorarc
        //this.strHTML = "<html><p>The net has inhibitor arc. Cannnot do analyse.</p></html>";
        //return;
        JPanel panel = new JPanel();

        panel.setLayout(new BoxLayout(panel,BoxLayout.Y_AXIS));
        JLabel lblAnalyse = new JLabel();
        
        if(this.rootNode == null){
            lblAnalyse.setText(ResourceBundle.getBundle("edu/uj/petri/messages").getString("Can't_analyse."));
            panel.add(lblAnalyse);
            return panel;
        }
        

        
        Generate(this.rootNode);
        this.model.applyMarking(this.initialMarking);
        
        // TODO sprawdz wlasnosci sieci: reachability & reversibility + strukturalne cuda
        strHTML += "<html>";
        if(this.isBoundness){
            strHTML += ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_is_<b>bounded</b>.</p>");
        }else{
            strHTML += ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_is_<b>not_bounded</b>.</p>");
        }
        
        if(isDead){
            strHTML += ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_has_<b>deadlock</b>.<p>");
        }else if(!isBoundness){
            
            strHTML += ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_has_<b>no_deadlocks</b>.</p>") +
                    //ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_is_<b>not_bounded</b>.</p>") +
                    ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_<b>might_be_deadlock_free.</b></p>");
            
        }else{
            strHTML += ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_has_<b>no_deadlocks</b>.</p>") +
                   //ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_is_<b>bounded</b>.</p>") +
                    ResourceBundle.getBundle("edu/uj/petri/messages").getString("<p>The_net_is_<b>deadlock_free.</b></p>");
        }
        
        strHTML += java.util.ResourceBundle.getBundle("edu/uj/petri/messages").getString("<br>Order_of_places_in_marking:<br>");

        for(Place p : model.getAllPlaces()){
            strHTML += "<b>" + p.getName() + "</b>, ";
        }
        
        strHTML += "</html>";
        
        
        DefaultMutableTreeNode root = new DefaultMutableTreeNode(this.rootNode.toString());
        AddNodesToTreeView(root,this.rootNode);
        
        JTree tree = new JTree(root);
        DefaultTreeCellRenderer renderer = new DefaultTreeCellRenderer();
        renderer.setLeafIcon(null);
        renderer.setClosedIcon(null);
        renderer.setOpenIcon(null);
        tree.setCellRenderer(renderer);
        expandAllNodesInJTree(tree);
        
        lblAnalyse.setText(this.strHTML);
        panel.add(lblAnalyse);
        JScrollPane treeView = new JScrollPane(tree);
        panel.add(treeView);
        
        return panel;
    }
    /** For internal use. Expands the tree view */
    private void expandAllNodesInJTree(JTree tree) {
        int row = 0;
        while (row < tree.getRowCount()) {
            tree.expandRow(row);
            row++;
        }
    }
    
}
